COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	boyerm[f82,jmc]		Note to Boyer and Moore about RSA proof
C00005 ENDMK
C⊗;
boyerm[f82,jmc]		Note to Boyer and Moore about RSA proof

	Thanks for "Proof checking the RSA Public Key Encryption
Algorithm".  It's very nice.  It would be nice to know how much
work it was, because that would measure our distance from being
able to advocate it as a routine tool replacing debugging.

	I have a nit to pick about your promise on page 3 to
verify a proof that CRYPT is easy to compute.  What you do is
to verify the ccrrectness of a fast version of CRYPT, but this
isn't quite the same.  Suppose you consider the amount work in
computing CRYPT to be the number of multiplications.  Then you
can use the "derived function" MULTS-IN-CRYPT defined by

MULTS-IN-CRYPT(M,e,n)
	=
if e is not a number or is 0,
	then 0
elseif e is even,
	then
	1 + MULTS-IN-CRYPT(M,e/2,n)
	else
	2 + MULTS-IN-CRYPT(M,e/2,n)

and use your standard methods to prove a statement about its
size.  The definition of MULTS-IN-CRYPT can be generated from the definition
of CRYPT by a program, and Ben Mozskowski wrote a few such LISP
functions a few years ago.  For any measure of work that interests
you, i.e. weighted sums of the numbers of certain operations and
the number of function calls, derived function generating programs
can be written.  Similar functions can be written for the amount
of storage used, etc.

	Anyway I think your prsentation could be made more convincing
by using MULTS-IN-CRYPT or something like it as the formalization of
RSA's first statement.  Any approach to verifying the third statement
would also involve derived functions of cryptogram solving programs.